Section: New Results

Encoding TLA⁺ proof obligations for SMT solvers

Participants : Stephan Merz, Hernán-Pablo Vanzetto.

The TLA⁺ proof system TLAPS (see 5.2 ) is being developed within a project at the MSR-INRIA Joint Centre in which we participate. The original release of TLAPS contained an SMT backend that handled quantifier-free proof obligations in linear arithmetic and that was occasionally useful, given that the other backends perform quite poorly on formulas involving arithmetic. However, TLA⁺ proof obligations usually mix arithmetic with other theories, in particular set theory, functions, records, and tuples. We propose a new encoding of TLA⁺ sequents in SMT-LIB, the generic input language of SMT solvers. The main challenge has been to design a sound translation from untyped TLA⁺ to the multi-sorted first-order logic that underlies SMT-LIB. We have developed a type system and a type inference algorithm that assigns SMT-LIB sorts to symbols and terms in the input formula, based on “typing assumptions” among the hypotheses present in the proof obligation.

The translation has been validated over several existing examples, yielding significant reductions in proof sizes. For example, the new backend can automatically verify the main invariant of a parameterized version of the Bakery algorithm, which previously required a few hundred lines of interactive proof. Similarly, an existing proof about a security architecture  [33] has been reduced by about 90%. The backend has been integrated in TLAPS and has been presented at a workshop [19] .